$\forall$${\it MA}$:MsgA, $s$:${\it MA}$.state, $k$:Knd, $l$:IdLnk, ${\it vaal}$:${\it MA}$.V($k$).
\\[0ex]$\neg$$\langle$$k$$,\,$$l$$\rangle$ $\in$ dom(1of(2of(2of(2of(2of(2of(${\it MA}$)))))))
\\[0ex]$\Rightarrow$ (filter($\lambda$${\it ms}$.eqof(IdLnkDeq)(mlnk(${\it ms}$),$l$);${\it MA}$.sends($k$,$s$,${\it vaal}$)) $\sim$ nil)